(declare-const si String)
(declare-const sj String)
(declare-const sk String)
(declare-const i Int)
(declare-const j Int)
(declare-const k Int)
(assert (= (str.to.int si) i))
(assert (= (str.to.int sj) j))
(assert (= (str.to.int sk) (* k k)))
(assert (= (- j i) k))
(assert (> i 7422885))
(assert (< j 74228850))
(assert (< i j))
(check-sat)
